The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0) → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0) → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0, c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0), c)
fold(t, x, 0) → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
foldB, f, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(6) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f, foldB, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(7) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f.

(8) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f', foldB, foldC, f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f'.

(10) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f'', foldB, foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f''.

(12) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldC, foldB, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)

Induction Base:
foldC(triple(0', 0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0', 0')

Induction Step:
foldC(triple(0', 0', 0'), gen_0':s4_0(+(n172_0, 1))) →_R^Ω(1)
f(foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)), C) →_IH
f(triple(gen_0':s4_0(c173_0), gen_0':s4_0(0), gen_0':s4_0(0)), C) →_R^Ω(1)
f'(triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), g(C)) →_R^Ω(1)
f'(triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(s(gen_0':s4_0(n172_0)), 0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_R^Ω(1)
f''(triple(s(gen_0':s4_0(n172_0)), 0', gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(s(gen_0':s4_0(n172_0)), 0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(s(gen_0':s4_0(n172_0)), 0', 0')

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldB, f, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Induction Base:
foldB(triple(0', 0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0', 0')

Induction Step:
foldB(triple(0', 0', 0'), gen_0':s4_0(+(n2892_0, 1))) →_R^Ω(1)
f(foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)), B) →_IH
f(triple(gen_0':s4_0(c2893_0), gen_0':s4_0(0), gen_0':s4_0(0)), B) →_R^Ω(1)
f'(triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), g(B)) →_R^Ω(1)
f'(triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(s(gen_0':s4_0(n2892_0)), 0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_R^Ω(1)
f''(triple(s(gen_0':s4_0(n2892_0)), 0', gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(s(gen_0':s4_0(n2892_0)), 0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(s(gen_0':s4_0(n2892_0)), 0', 0')

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f, foldC, f', f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f.

(20) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f', foldC, f'', fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f'.

(22) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
f'', foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol f''.

(24) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
foldC, fold

They will be analysed ascendingly in the following order:
foldB = f
foldB = foldC
foldB = f'
foldB = f''
f = foldC
f = f'
f = f''
f < fold
foldC = f'
foldC = f''
f' = f''

(25) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)

Induction Base:
foldC(triple(0', 0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0', 0')

Induction Step:
foldC(triple(0', 0', 0'), gen_0':s4_0(+(n5686_0, 1))) →_R^Ω(1)
f(foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)), C) →_IH
f(triple(gen_0':s4_0(c5687_0), gen_0':s4_0(0), gen_0':s4_0(0)), C) →_R^Ω(1)
f'(triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), g(C)) →_R^Ω(1)
f'(triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(s(gen_0':s4_0(n5686_0)), 0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_R^Ω(1)
f''(triple(s(gen_0':s4_0(n5686_0)), 0', gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(s(gen_0':s4_0(n5686_0)), 0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(s(gen_0':s4_0(n5686_0)), 0', 0')

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(26) Complex Obligation (BEST)

(27) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

The following defined symbols remain to be analysed:
fold

(28) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
fold(triple(0', 0', 0'), A, gen_0':s4_0(n8455_0)) → triple(gen_0':s4_0(n8455_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n8455₀)

Induction Base:
fold(triple(0', 0', 0'), A, gen_0':s4_0(0)) →_R^Ω(1)
triple(0', 0', 0')

Induction Step:
fold(triple(0', 0', 0'), A, gen_0':s4_0(+(n8455_0, 1))) →_R^Ω(1)
f(fold(triple(0', 0', 0'), A, gen_0':s4_0(n8455_0)), A) →_IH
f(triple(gen_0':s4_0(c8456_0), gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f'(triple(gen_0':s4_0(n8455_0), gen_0':s4_0(0), gen_0':s4_0(0)), g(A)) →_R^Ω(1)
f'(triple(gen_0':s4_0(n8455_0), gen_0':s4_0(0), gen_0':s4_0(0)), A) →_R^Ω(1)
f''(foldB(triple(s(gen_0':s4_0(n8455_0)), 0', gen_0':s4_0(0)), gen_0':s4_0(0))) →_R^Ω(1)
f''(triple(s(gen_0':s4_0(n8455_0)), 0', gen_0':s4_0(0))) →_R^Ω(1)
foldC(triple(s(gen_0':s4_0(n8455_0)), 0', 0'), gen_0':s4_0(0)) →_R^Ω(1)
triple(s(gen_0':s4_0(n8455_0)), 0', 0')

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(29) Complex Obligation (BEST)

(30) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)
fold(triple(0', 0', 0'), A, gen_0':s4_0(n8455_0)) → triple(gen_0':s4_0(n8455_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n8455₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(31) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)

(32) BOUNDS(n^1, INF)

(33) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)
fold(triple(0', 0', 0'), A, gen_0':s4_0(n8455_0)) → triple(gen_0':s4_0(n8455_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n8455₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(34) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)

(35) BOUNDS(n^1, INF)

(36) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(37) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0', 0'), gen_0':s4_0(n5686_0)) → triple(gen_0':s4_0(n5686_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n5686₀)

(38) BOUNDS(n^1, INF)

(39) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)
foldB(triple(0', 0', 0'), gen_0':s4_0(n2892_0)) → triple(gen_0':s4_0(n2892_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n2892₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(40) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)

(41) BOUNDS(n^1, INF)

(42) Obligation:

Innermost TRS:
Rules:
g(A) → A
g(B) → A
g(B) → B
g(C) → A
g(C) → B
g(C) → C
foldB(t, 0') → t
foldB(t, s(n)) → f(foldB(t, n), B)
foldC(t, 0') → t
foldC(t, s(n)) → f(foldC(t, n), C)
f(t, x) → f'(t, g(x))
f'(triple(a, b, c), C) → triple(a, b, s(c))
f'(triple(a, b, c), B) → f(triple(a, b, c), A)
f'(triple(a, b, c), A) → f''(foldB(triple(s(a), 0', c), b))
f''(triple(a, b, c)) → foldC(triple(a, b, 0'), c)
fold(t, x, 0') → t
fold(t, x, s(n)) → f(fold(t, x, n), x)

Types:
g :: A:B:C → A:B:C
A :: A:B:C
B :: A:B:C
C :: A:B:C
foldB :: triple → 0':s → triple
0' :: 0':s
s :: 0':s → 0':s
f :: triple → A:B:C → triple
foldC :: triple → 0':s → triple
f' :: triple → A:B:C → triple
triple :: 0':s → 0':s → 0':s → triple
f'' :: triple → triple
fold :: triple → A:B:C → 0':s → triple
hole_A:B:C1_0 :: A:B:C
hole_triple2_0 :: triple
hole_0':s3_0 :: 0':s
gen_0':s4_0 :: Nat → 0':s

Lemmas:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)

Generator Equations:
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))

No more defined symbols left to analyse.

(43) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
foldC(triple(0', 0', 0'), gen_0':s4_0(n172_0)) → triple(gen_0':s4_0(n172_0), gen_0':s4_0(0), gen_0':s4_0(0)), rt ∈ Ω(1 + n172₀)

(44) BOUNDS(n^1, INF)